Design of modern digital circuits is accomplished with electronic design automation (EDA) tools, capable of dealing with component arrays that total millions of gates. Such systems are well beyond the capacity of human designers. Generally, an EDA tool must be able to accept as input a functional description of a given circuit, and it must produce as output a concrete circuit design. The art has largely relied on hardware design languages (HDLs) to perform automated electronic design functions. Languages such as Verilog or VHDL can express designs either at gate level or at Register Transfer Level (RTL). After the design is rendered in RTL, the design is translated into a combinational netlist, which can serve as a blueprint for rendering the circuit in silicon.
A major issue, however, is the need to validate such a circuit. Not only must the designer be confident of the ability of the circuit to operate without electronic, timing or interconnection issues, but the designer must also verify that the circuit performs the logical operations specified. The most common approach to such verification is to simulate the actual circuit operation. Simulation routines commonly employed in the art are discrete operations—inputs are presented, the circuit response is simulated, and outputs are determined. Such simulation here is referred to as “concrete”, as the simulation consists of providing concrete signal values—1's and 0's—to the device under test (DUT), and then collecting the responses.
The primary weakness of concrete simulation is the necessity for a designer to construct the simulation routines. Nothing can be tested under such a system unless the appropriate inputs are determined and presented to the DUT. That is, the designer must anticipate how to conduct the test—exactly what test, how to test it, and the inputs required. Given the complexity of a modern digital circuit, no system could run all possible inputs, and no designer could list them. Thus, the completeness of the test depends on the skill of the test designer, not the capability of the test system.
In addition, concrete simulation tests one cycle of DUT operation for each cycle of simulation. Of course, simulation of a complex circuit proceeds at a relatively slow pace, given the need to determine and record operations across a circuit. Actual rates of 1 hz are not uncommon. Given that the DUT will generally be designed to operate in the gigahertz range, the physical impossibility of performing exhaustive and complete concrete testing is clear.
Model checking provides the exhaustive verification not possible with concrete methods. Such model checking requires gate-level netlists, however, and systems available in the art for performing such translation are generally limited in the range of HDL RTL language constructs that can be represented. Moreover, they do not fully preserve the behavior and semantics of the HDL RTL after translation. Those issues are addressed in the system set out below.